\section{M\'odulo DiccionarioT(nombre, $\alfa$)}

\subsection{Servicios Exportados}

\subsubsection{Interfaz \nombretad{DiccionarioT(nombre, $\alfa$)}}
\begin{onehalfspace}
\textbf{\bf g\'enero:} diccT

\textbf{\bf usa interfaces:} \nombretad{Nombre}, \nombretad{Conjunto}, \nombretad{Arreglo}, \nombretad{Puntero}, \nombretad{$\alpha$}, \nombretad{$\beta$}

\textbf{\bf se explica con :} \nombretad{dicc(nombre, $\alfa$)}

\noindent \textbf{operaciones:}
\end{onehalfspace}
\vspace{0.5cm}

%---------------------------------------------------------------
\noindent
\f{VacioT}() \en $res$: \g{diccT} \\
\indent $ \{  True \}\ $ \\
\indent $ \{ \sombrero{res} \equiv vacio \} $ \\


%---------------------------------------------------------------

\noindent
\f{DefT?}(in \:n : nombre, in \:d: diccT) \en $res$: \g{bool} \\
\indent $ \{  True \}\ $ \\
\indent $ \{ \sombrero{res} \equiv def?(\sombrero{n}, \sombrero{d}) \}\ $ \\

%---------------------------------------------------------------

%---------------------------------------------------------------
\noindent
\f{DefinirT}( in n: nombre,  in s: $\alfa$, inout \:d: diccT)  \\
\indent $ \{ \sombrero{d} \equiv d_0\} $ \\
\indent $ \{\sombrero{d} \equiv definir(\sombrero{n}, \sombrero{s}, d_0) \} $ \\

%---------------------------------------------------------------


%---------------------------------------------------------------
\noindent
\f{ObtenerT}(in n: nombre, in \:d: diccT) \en $res$: \g{$\alfa$} \\
\indent $ \{ def?(\sombrero{n}, \sombrero{d}) \} $ \\
\indent $ \{ \sombrero{res} \equiv obtener(\sombrero{n}, \sombrero{d}) \} $ \\

%---------------------------------------------------------------

%---------------------------------------------------------------
\noindent
\f{ClavesT}(in d: diccT) \en $res$: \g{conj(nombre)} \\
\indent $ \{ True \} $ \\
\indent $ \{ \sombrero{res} \equiv claves( \sombrero{d}) \} $ \\

%---------------------------------------------------------------

\subsubsection{Aspectos de Aliasing}
\begin{itemize}
\item Obtener devuelve una referncia a una variable de tipo $\alfa$. La misma no debe ser modificada. Para modificar el valor de un item debe utilizarse el m�todo \textit{Definir}
\item Definir modifica  al diccionario pasado como par\'ametro.	
\item Claves devuelve una referencia al conjunto de claves del diccionario. El mismo no debe ser modificado.
\end{itemize}

\subsubsection{Ordenes de Complejidad}

\begin{itemize}
\item \orden{Vacio}{O(1)}
\item \orden{Def?}{long(n)}
\item \orden{Definir}{long(n)}
\item \orden{Obtener}{long(n)}
\item \orden{Claves}{O(1)}
\end{itemize}
donde long(n) es la longitud del nombre (cantidad de caracteres)
\newpage
\subsection{Representaci\'on}

\subsubsection{Estructura de Representaci\'on}

\begin{onehalfspace}

	$diccT$ src {\bf estrDT[cantSimbolos\footnote{cantSimbolos es la cantidad de simbolos permitidos en el alfabeto}]}, donde {\bf estrDT} es

	\indent \indent tupla  $<$ raiz : trie $\times$ claves: conj($\alfa$) $>$

donde {\bf trie} es \\
\indent \indent {tupla $<$ hijos[cantSimbolos] : arreglo(puntero(trie)) $\times$ significado: puntero($\beta$) $>$}

\end{onehalfspace}

\vspace{0.2cm}

\subsubsection{Invariante de Representaci\'on}

Rep: $\sombrero{estrDT}$ $\longrightarrow boolean $
$(\forall e: \sombrero{estrDT})\,Rep(e) \equiv$

\begin{enumerate}
\item[\color{blue}{\fbox{1}}]{($\forall$ n: nombre)(esta?(n, e.claves) $\Leftrightarrow$ defEnTrie(n, e.diccionario)} 
\item[\color{blue}{\fbox{2}}]{$esTrie(e.diccionario)$} 
\end{enumerate}

\textbf{donde}

esTrie: trie $\longrightarrow$ bool \\
$(\forall t: trie\, esTrie(e) \equiv$
\begin{enumerate}
\item[\color{blue}{\fbox{3}}]{$noTieneDuplicados(t)$} 
\item[\color{blue}{\fbox{4}}]{$noTieneCiclos(t)$} 
\item[\color{blue}{\fbox{5}}]{$t.significado \neq NULL \vee (\exists i: nat) (i < cantSimbolos \yluego t.hijos[i] \neq NULL) $}
\item[\color{blue}{\fbox{6}}]{($\forall$ i: nat)$\big($ i $<$ cantSimbolos $\impluego$ (t.hijos[i] = NULL $\oluego$ esTrie(t.hijos[i]) $\big)$)} 
\end{enumerate}

\textbf{donde}

noTieneDuplicados: arreglo(puntero(trie): v[cantSimbolos] $\longrightarrow$ bool \\
noTieneDuplicados(v) $\equiv$ \\
\indent ($\forall$ i, j: nat)(i $<$ cantSimbolos $\wedge$ j $<$ cantSimbolos) $\impluego$ \\
\indent\indent $\big($(v[i] = null] $\wedge$ v[j] = null) $\vee$ (v[i] $\neq$ v[j]) $\big)$
\\
\\
noTieneCiclos: puntero(trie) t $\times$ conj(puntero(trie) yaRecorridos $\longrightarrow$ bool \\
noTieneCiclos(t, yaRecorridos) $\equiv$ (t=null) $\oluego$ \\
\indent $\big($ $\neg$esta?(t, yaRecorridos) $\wedge$ \\
\indent\indent ($\forall$ i: nat)(i < cantSimbolos) $\impluego$ noTieneCiclos(t$\rightarrow$hijos[i], agregar(t, yaRecorridos)) $\big)$ \\
\\
\\
defEnTrie: trie t $\times$ nombre n $\longrightarrow$ bool \\
defEnTrie(t,n) $\equiv$ \\
\textbf{if} long(n) = 1 \\
\indent \textbf{then} $\big($ t.hijos[$\textit{CharToNat}$(prim(n))] $\neq$ NULL) $\yluego$ \\
\indent\indent\indent t.hijos[$\textit{CharToNat}$(prim(n))]$\rightarrow$significado $\neq$ NULL $\big)$ \\
\indent \textbf{else}  $\big($ t.hijos[$\textit{CharToNat}$(prim(n))] $\neq$ NULL) $\yluego$ \\
\indent\indent\indent $\textit{defEnTrie}$(t.hijos[$\textit{CharToNat}$(prim(n))], fin(n)) $\big)$ \\
\textbf{endif}
\newpage
    						
\subsubsection{Explicaciones del Invariante}
\begin{enumerate}
\item[\color{blue}{\fbox{1}}] {Todos los elementos del conjunto de claves est�n en el trie, y todas las claves del trie est�n en el conjunto de claves.}
\item[\color{blue}{\fbox{2}}] {El trie es v�lido.}
\end{enumerate}
Donde ser un trie v�lido significa que:
\begin{enumerate}
\item[\color{blue}{\fbox{3}}] {No hay duplicados en el arreglo de hijos (no hay dos hijos que sean la misma referencia - notar que s� pueden ser observacionalmente iguales}
\item[\color{blue}{\fbox{4}}] {El trie no tiene ciclos.}
\item[\color{blue}{\fbox{5}}] {Si un nodo no tiene hijos debe tener significado, y si no tiene significado debe tener al menos un hijo.}
\item[\color{blue}{\fbox{6}}] {Todos los elementos del arreglo de hijos son tries v�lidos.}
\end{enumerate}
\vspace{0.3cm}


\subsubsection{Funci\'on de Abstracci\'on}
\begin{onehalfspace}
($\forall$ t: trie) Abs(t) = d: dicc(nombre, $\alfa$) /\\
\indent\indent($\forall$ n : nombre) def?(n, d) = defEnTrie(n, t)$\wedge$ \\
\indent\indent($\forall$ n : nombre) def?(n, d) $\impluego$ obtener(n, d) = obtenerDelTrie(n,t)\\
\end{onehalfspace}
donde: \\
defEnTrie es la funci�n definida anteriormente, y
\\
\\
obtenerDelTrie: trie t $\times$ nombre n $\longrightarrow$ $\beta$ \indent\indent\indent (defEnTrie(t,n)) \\
obtenerDelTrie(t,n) $\equiv$ \\
\textbf{if} long(n) = 1 \\
\indent \textbf{then} t.hijos[\textit{CharToNat}(prim(n))]$\rightarrow$significado \\
\indent \textbf{else} \textit{obtenerDelTrie}(t.hijos[\textit{CharToNat}(prim(n))], fin(n))

\newpage

\subsection{Operaciones}

\subsubsection{Algoritmos}

\begin{algorithm}{\it iVacioT}{}{res : estrDT}
		\VAR {t: trie} \\
		\VAR (i: nat) \\
		\VAR {hijos: arreglo(puntero(trie))} \\
		\comentario{\color{blue} Se crea el arreglo de hijos}\\
		hijos \= crearArreglo[cantSimbolos] \\
		i \= 0 \\
		\comentario{\color{blue} Se inicializa el arreglo en NULL.}\\
		\begin{WHILE}{i < cantSimbolos}
			hijos[i] \= NULL
		\end{WHILE} \\
		t \= tupla<hijos, $\textit{SIGNIFICADO\_RAIZ}$>	 \\
		res \= tupla<t, vacio>
\end{algorithm}


\begin{algorithm}{\it iDefinirT}{\param{in}{n} {nombre}, \param{in}{signif}{$\alfa$}, \param {inout}{d}{estrDT}}{}
	\VAR{pTrie : puntero(trie)}\\
	\VAR{codChar: nat}\\
	\VAR{itNombre: iterSecu}\\
	itNombre \= crearIt(n)\\
	\\
	pTrie\= $\&$(d.trie)
	\\
	\begin{WHILE}{tieneProximo(itNombre)}
		codChar \= CharToNat(proximo(itNombre))\\
		\begin{IF}{pTrie \rightarrow hijos[codChar] ==  NULL}
			(pTrie \rightarrow hijos[codChar]) \= vacio
		\end{IF}
		pTrie \= (pTrie \rightarrow hijos[codChar])
		\\
		\begin{IF}{\neg tieneProximo(itNombre)}
			(pTrie \rightarrow significado) \= signif
		\end{IF}
	\end{WHILE}
	\\
	agregar(n, d.claves)		
\end{algorithm}

\begin{algorithm}{\it idefT?} {\param{in}{n}{nombre}, \param {in}{d}{trie}} {res: bool}
	\VAR{pTrie : puntero(trie)}\\
	\VAR{codChar: nat} \\
	\VAR{seguir: bool}\\
	\VAR{itNombre: iterSecu}\\	
	itNombre \= crearIt(n)\\
	pTrie\= $\&$ (d.raiz) \\
	sigue \= true\\
	res \= false \\
	\begin{WHILE}{tieneProximo(itNombre) \wedge seguir }
		codChar \= CharToNat(proximo(itNombre))\\
		\begin{IF}{pTrie \rightarrow hijos[codChar] == NULL}
			seguir \= false
		\ELSE 
			pTrie \= (pTrie \rightarrow hijos[codChar] \\
			\begin{IF}{\neg tieneProximo(itNombre)}
				res \= (pTrie \rightarrow significado \neq NULL)
			\end{IF}
		\end{IF}		
	\end{WHILE}
\end{algorithm}

\begin{algorithm}{\it iobtenerT} {\param{in}{n}{nombre}, \param {in}{d}{trie}} {res: \alfa}
	\VAR{pTrie : puntero(trie)}\\
	\VAR{codChar: nat} \\
	\VAR{itNombre: iterSecu}\\	
	itNombre \= crearIt(n)\\
	pTrie\= $\&$ (d.raiz) \\
	\\
	\begin{WHILE}{tieneProximo(itNombre)}
		codChar \= CharToNat(proximo(itNombre))\\
		pTrie \= (pTrie \rightarrow hijos[codChar] \\
		\begin{IF}{\neg tieneProximo(itNombre)}
			res \= pTrie \rightarrow significado		
		\end{IF}		
	\end{WHILE}
\end{algorithm}

\begin{algorithm}{\it iclavesT} {\param {in}{d}{trie}} {res: conj(nombre)}
	res \= d.claves
\end{algorithm}


\newpage

\subsubsection{Explicaci\'on de los \'ordenes de complejidad}
\begin{itemize}
\item \justorden {vacioT}{Primero, la funci\'on crear arreglo es de orden $O(tamano)$, pero como en este caso el tama\~no es la constante fija $cantSimbolos$ (cantidad de s\'imbolos) la operaci\'on es de orden constante. Se asume que la operaci\'on de crear el arreglo es de orden constante, as\'i como las operaciones de asignaci\'on.  Por \'ultimo, se inicializan los valores dentro de arreglo, en un ciclo que se ejecuta $cantSimbolos$ veces. Como dentro del ciclo s\'olo se realiza una asignaci\'on, esta operaci\'on ser\'a de orden constante. Por lo tanto la funci\'on vacioT es $O(1)$ }
\item \justorden {definirT}{Para definir una clave determinada, es necesario iterar los caracteres del nombre \textit{n}. Por lo tanto, el ciclo se ejecutar\'a \textit{long(n)} veces, donde \textit{long(n)} es la longitud en caracteres del nombre. Dentro del ciclo, se observa que las operaciones realizadas son todas $O(1)$, dado que se asumi\'o que la funci�n \textit{CharToNat} es $O(1)$, u que las operaciones sobre los iteradores de secuencia se realizan en $O(1)$. Luego, como la inserci\'on del nombre en el conjunto de claves es $O(1)$, la funci\'on tiene complejidad $O(long(n))$ }
\item \justorden {defT?}{Por lo mencionado en el \'item  anterior, las asignaciones previas al ciclo se realizan en $o(1)$. Como es de inter\'es el peor caso, asumiremos que el ciclo se ejecuta el n\'umero m\'aximo posible de veces, lo cual ser\'ia \textit{long(n)} veces. Dentro del ciclo se realizan operaciones que son todas $O(1)$, teniendo en cuenta las mismas aclaraciones realizadas en el \'item anterior. Por lo tanto, la complejidad de la funci�n ser\'a $O(long(n))$}
\item \justorden {obtenerT}{ Para obtener un elemento del trie, es necesario iterar la totalidad de caracteres de su clave. Esto implica realizar un ciclo que se ejecuta \textit{long(n)} veces. Como se indic� anteriormente, las operaciones sobre iteradores de secuencias se realizan en $O(1)$. Teniendo en cuenta esto, y que el resto de las operaciones dentro del ciclo son simples asignaciones, puede determinarse que la complejidad de esta funci\'on es $O(long(n))$.}
\item \justorden {clavesT}{Dado que esta fuci\'on devuelve el conjunto de claves haciendo aliasing, su orden de complejidad ser\'a $O(1)$.}

\end{itemize}

\subsection{Servicios Usados}
Se asumi� la existencia de una constante \textit{SIGNIFICADO\_RAIZ}. La misma es el significado que debe establecerse al nodo ra�z del trie, para mantener el invariante de representaci�n. Dicho valor carecer\'a de sentido para las claves del diccionario.
\subsubsection{\nombretad{Nombre}}
Se asume que:
\begin{itemize}
\item{Un nombre es una secuencia no vacia de caracteres.}
\item{Est\'a dado un nat $cds$ que denota la cantidad de s\'imbolos permitidos en nuestro alfabeto.}
\item{Existen una funci\'on $CharToNat$ que mapea un nat i con el i-\'esimo caracter del alfabeto, empezando por 0. Su comlejidad es $O(1)$}
\item{Se asume que las funciones con iteradores de secuencia se realizan en $O(1)$} 
\end{itemize}

\subsubsection{\nombretad{Conjunto}}
Se requiere que las operaciones tengan los siguientes \'ordenes:
\begin{itemize}
\item VacioC: $O(1)$
\item AgregarC: $O(1)$
\end{itemize}

\subsubsection{\nombretad{Arreglo}}
Se requiere que:
\begin{itemize}
\item {La operaci\'on de creaci\'on de un arreglo sea de orden $O(tam)$ donde tam es el tama�o del arreglo a definir}
\item {La operaci\'on de indexaci\'on tenga orden $O(1)$}
\item {La operaci\'on de asignaci\'on a una posici\'on sea $O(1)$}
\item{La operaci\'on tam tenga orden $O(1)$ }
\end{itemize}
